package alloy.transform.atomize;

import java.util.Iterator;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.ComprehensionExpr;
import alloy.ast.LeafExpr;
import alloy.ast.Node;
import alloy.ast.QuantifiedFormula;
import alloy.ast.SigExpr;
import alloy.ast.SumIntExpr;
import alloy.ast.TypedExpr;
import alloy.ast.VarCreator;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.type.UnionType;
import alloy.util.Dbg;

/**
 * 
 * for debugging purposes--checks if all expressions' types are atomic
 */
class AtomizationCheckVisitor extends ASTDepthFirstVisitor {

	private CommandState info;

	AtomizationCheckVisitor(final CommandState info) {
		this.info = info;
	}

	public void visit(ComprehensionExpr compExpr_) {
		visit((VarCreator) compExpr_);
	}

	public void visit(QuantifiedFormula quantForm_) {
		visit((VarCreator) quantForm_);
	}

	public void visit(SigExpr sigExpr_) {
		visit((TypedExpr) sigExpr_);
	}

	public void visit(SumIntExpr sumIntExpr_) {
		visit((VarCreator) sumIntExpr_);
	}

	public void visit(TypedExpr expr) {
		UnionType type = expr.getType();
		Dbg.chk(type.size() == 1,
				"type of expr still a union after atomization: " + expr
						+ " , type: " + type);
		RelationType relType = type.toRelationType();
		for (Iterator typesIter = relType.getTypeIter(); typesIter.hasNext();) {
			BasicType basType = (BasicType) typesIter.next();
			Dbg.chk(info._atomicTypes.contains(basType),
					"non-atomic type found after atomization: " + expr
							+ " , type: " + type);
		}

		if (expr instanceof LeafExpr) {
			Dbg.chk(((LeafExpr) expr).getLeafId());
		}
	}

	public void visit(VarCreator varCreator_) {
		Dbg.chk(varCreator_.getLeafIdMap());
		visit((Node) varCreator_);
	}
}
